WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1 ,Zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1,cond_eval_expr_2,cond_eval_expr_3,eval#1 ,main} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) cond_eval_expr_3#(Zero(),x5) -> c_6() eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Nat(x4)) -> c_8() eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) cond_eval_expr_3#(Zero(),x5) -> c_6() eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Nat(x4)) -> c_8() eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6,8} by application of Pre({6,8}) = {2,3,4,7,9,10}. Here rules are labelled as follows: 1: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) 2: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) 3: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) 4: cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) 5: cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) 6: cond_eval_expr_3#(Zero(),x5) -> c_6() 7: eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) 8: eval#1#(Nat(x4)) -> c_8() 9: eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) 10: main#(x0) -> c_10(eval#1#(x0)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak DPs: cond_eval_expr_3#(Zero(),x5) -> c_6() eval#1#(Nat(x4)) -> c_8() - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 2:S:cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 eval#1#(Nat(x4)) -> c_8():10 3:S:cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))):5 -->_2 eval#1#(Nat(x4)) -> c_8():10 -->_1 cond_eval_expr_3#(Zero(),x5) -> c_6():9 4:S:cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 eval#1#(Nat(x4)) -> c_8():10 5:S:cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 6:S:eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Nat(x4)) -> c_8():10 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)):2 -->_1 cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))):1 7:S:eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) -->_2 eval#1#(Nat(x4)) -> c_8():10 -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)):4 -->_1 cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)):3 8:S:main#(x0) -> c_10(eval#1#(x0)) -->_1 eval#1#(Nat(x4)) -> c_8():10 -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 9:W:cond_eval_expr_3#(Zero(),x5) -> c_6() 10:W:eval#1#(Nat(x4)) -> c_8() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: cond_eval_expr_3#(Zero(),x5) -> c_6() 10: eval#1#(Nat(x4)) -> c_8() * Step 4: RemoveHeads WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 2:S:cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 3:S:cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))):5 4:S:cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 5:S:cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 6:S:eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)):2 -->_1 cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))):1 7:S:eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)):4 -->_1 cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)):3 8:S:main#(x0) -> c_10(eval#1#(x0)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(8,main#(x0) -> c_10(eval#1#(x0)))] * Step 5: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 6: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Add :: ["A"(4) x "A"(4)] -(0)-> "A"(4) Add :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Nat :: ["A"(0)] -(0)-> "A"(0) Nat :: ["A"(0)] -(0)-> "A"(13) Nat :: ["A"(0)] -(0)-> "A"(14) Nat :: ["A"(0)] -(0)-> "A"(10) Nat :: ["A"(0)] -(0)-> "A"(15) Nat :: ["A"(0)] -(0)-> "A"(7) Sub :: ["A"(4) x "A"(4)] -(4)-> "A"(4) Sub :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Succ :: ["A"(0)] -(0)-> "A"(0) Succ :: ["A"(0)] -(0)-> "A"(3) Zero :: [] -(0)-> "A"(0) Zero :: [] -(0)-> "A"(7) cond_eval_expr_1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) cond_eval_expr_2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) cond_eval_expr_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) eval#1 :: ["A"(0)] -(0)-> "A"(0) cond_eval_expr_1# :: ["A"(0) x "A"(4)] -(0)-> "A"(0) cond_eval_expr_2# :: ["A"(0) x "A"(4)] -(4)-> "A"(8) cond_eval_expr_3# :: ["A"(0) x "A"(0)] -(4)-> "A"(13) eval#1# :: ["A"(4)] -(0)-> "A"(1) c_1 :: ["A"(1)] -(0)-> "A"(1) c_2 :: ["A"(0)] -(0)-> "A"(12) c_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(12) c_4 :: ["A"(0)] -(0)-> "A"(12) c_5 :: ["A"(0)] -(0)-> "A"(15) c_7 :: ["A"(0) x "A"(0)] -(0)-> "A"(12) c_9 :: ["A"(1) x "A"(0)] -(0)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Add_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "Nat_A" :: ["A"(0)] -(0)-> "A"(1) "Sub_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "Succ_A" :: ["A"(0)] -(0)-> "A"(1) "Zero_A" :: [] -(0)-> "A"(1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_4_A" :: ["A"(0)] -(0)-> "A"(1) "c_5_A" :: ["A"(0)] -(0)-> "A"(1) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) 2. Weak: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 7: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Add :: ["A"(2) x "A"(2)] -(2)-> "A"(2) Add :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Nat :: ["A"(0)] -(0)-> "A"(0) Nat :: ["A"(0)] -(0)-> "A"(12) Nat :: ["A"(0)] -(0)-> "A"(14) Nat :: ["A"(0)] -(0)-> "A"(10) Nat :: ["A"(0)] -(0)-> "A"(2) Nat :: ["A"(0)] -(0)-> "A"(8) Nat :: ["A"(0)] -(0)-> "A"(4) Sub :: ["A"(2) x "A"(2)] -(0)-> "A"(2) Sub :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Sub :: ["A"(8) x "A"(8)] -(0)-> "A"(8) Succ :: ["A"(0)] -(0)-> "A"(0) Succ :: ["A"(0)] -(0)-> "A"(2) Zero :: [] -(0)-> "A"(0) Zero :: [] -(0)-> "A"(15) cond_eval_expr_1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) cond_eval_expr_2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) cond_eval_expr_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) eval#1 :: ["A"(0)] -(0)-> "A"(0) cond_eval_expr_1# :: ["A"(0) x "A"(2)] -(2)-> "A"(2) cond_eval_expr_2# :: ["A"(0) x "A"(2)] -(0)-> "A"(1) cond_eval_expr_3# :: ["A"(0) x "A"(0)] -(0)-> "A"(9) eval#1# :: ["A"(2)] -(0)-> "A"(12) c_1 :: ["A"(0)] -(0)-> "A"(10) c_2 :: ["A"(0)] -(0)-> "A"(10) c_3 :: ["A"(0) x "A"(1)] -(0)-> "A"(1) c_4 :: ["A"(0)] -(0)-> "A"(4) c_5 :: ["A"(0)] -(0)-> "A"(14) c_7 :: ["A"(0) x "A"(0)] -(0)-> "A"(14) c_9 :: ["A"(0) x "A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "Nat_A" :: ["A"(0)] -(0)-> "A"(1) "Sub_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "Succ_A" :: ["A"(0)] -(0)-> "A"(1) "Zero_A" :: [] -(0)-> "A"(1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_4_A" :: ["A"(0)] -(0)-> "A"(1) "c_5_A" :: ["A"(0)] -(0)-> "A"(1) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) 2. Weak: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 8: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Add :: ["A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8) Add :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) Nat :: ["A"(8, 0)] -(0)-> "A"(8, 0) Nat :: ["A"(8, 0)] -(0)-> "A"(8, 14) Nat :: ["A"(8, 0)] -(0)-> "A"(8, 8) Nat :: ["A"(8, 0)] -(0)-> "A"(8, 3) Nat :: ["A"(8, 0)] -(0)-> "A"(8, 1) Sub :: ["A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8) Sub :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) Succ :: ["A"(8, 0)] -(8)-> "A"(8, 0) Succ :: ["A"(8, 0)] -(8)-> "A"(8, 10) Zero :: [] -(0)-> "A"(8, 0) Zero :: [] -(0)-> "A"(8, 8) cond_eval_expr_1 :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) cond_eval_expr_2 :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) cond_eval_expr_3 :: ["A"(8, 0) x "A"(8, 0)] -(8)-> "A"(8, 0) eval#1 :: ["A"(8, 0)] -(0)-> "A"(8, 0) cond_eval_expr_1# :: ["A"(8, 0) x "A"(8, 8)] -(0)-> "A"(2, 0) cond_eval_expr_2# :: ["A"(8, 0) x "A"(8, 8)] -(0)-> "A"(1, 4) cond_eval_expr_3# :: ["A"(8, 0) x "A"(8, 0)] -(4)-> "A"(1, 0) eval#1# :: ["A"(0, 8)] -(0)-> "A"(4, 0) c_1 :: ["A"(0, 0)] -(0)-> "A"(4, 12) c_2 :: ["A"(0, 0)] -(0)-> "A"(3, 0) c_3 :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 6) c_4 :: ["A"(0, 0)] -(0)-> "A"(12, 14) c_5 :: ["A"(0, 0)] -(0)-> "A"(1, 0) c_7 :: ["A"(2, 0) x "A"(2, 0)] -(0)-> "A"(4, 2) c_9 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(8, 6) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Add_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "Add_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "Nat_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "Nat_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "Sub_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "Sub_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "Succ_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "Succ_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "Zero_A" :: [] -(0)-> "A"(1, 0) "Zero_A" :: [] -(0)-> "A"(0, 1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_2_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) "c_4_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_4_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_5_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_5_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) 2. Weak: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 9: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Add :: ["A"(11, 11) x "A"(0, 11)] -(11)-> "A"(0, 11) Add :: ["A"(11, 0) x "A"(11, 0)] -(0)-> "A"(11, 0) Nat :: ["A"(11, 0)] -(0)-> "A"(11, 0) Nat :: ["A"(11, 0)] -(0)-> "A"(11, 14) Nat :: ["A"(11, 0)] -(0)-> "A"(11, 1) Nat :: ["A"(11, 0)] -(0)-> "A"(11, 12) Nat :: ["A"(11, 0)] -(0)-> "A"(11, 11) Sub :: ["A"(11, 11) x "A"(11, 11)] -(11)-> "A"(0, 11) Sub :: ["A"(11, 0) x "A"(11, 0)] -(11)-> "A"(11, 0) Succ :: ["A"(11, 0)] -(11)-> "A"(11, 0) Succ :: ["A"(11, 0)] -(11)-> "A"(11, 6) Zero :: [] -(0)-> "A"(11, 0) Zero :: [] -(0)-> "A"(11, 8) cond_eval_expr_1 :: ["A"(11, 0) x "A"(11, 0)] -(0)-> "A"(11, 0) cond_eval_expr_2 :: ["A"(11, 0) x "A"(11, 0)] -(0)-> "A"(11, 0) cond_eval_expr_3 :: ["A"(11, 0) x "A"(11, 0)] -(7)-> "A"(11, 0) eval#1 :: ["A"(11, 0)] -(0)-> "A"(11, 0) cond_eval_expr_1# :: ["A"(11, 0) x "A"(0, 11)] -(6)-> "A"(5, 13) cond_eval_expr_2# :: ["A"(11, 0) x "A"(11, 11)] -(1)-> "A"(4, 4) cond_eval_expr_3# :: ["A"(11, 0) x "A"(11, 0)] -(4)-> "A"(0, 0) eval#1# :: ["A"(0, 11)] -(1)-> "A"(14, 0) c_1 :: ["A"(0, 0)] -(0)-> "A"(7, 15) c_2 :: ["A"(0, 0)] -(0)-> "A"(5, 14) c_3 :: ["A"(0, 0) x "A"(10, 0)] -(0)-> "A"(11, 10) c_4 :: ["A"(0, 0)] -(0)-> "A"(4, 4) c_5 :: ["A"(0, 0)] -(0)-> "A"(0, 0) c_7 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 15) c_9 :: ["A"(0, 0) x "A"(0, 0)] -(1)-> "A"(14, 1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Add_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "Add_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1) "Nat_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "Nat_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "Sub_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "Sub_A" :: ["A"(1, 1) x "A"(1, 1)] -(1)-> "A"(0, 1) "Succ_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "Succ_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "Zero_A" :: [] -(0)-> "A"(1, 0) "Zero_A" :: [] -(0)-> "A"(0, 1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_2_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) "c_4_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_4_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_5_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_5_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_9_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) 2. Weak: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) * Step 10: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) - Weak DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3# ,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Add :: ["A"(3, 3) x "A"(0, 3)] -(3)-> "A"(0, 3) Add :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 0) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 6) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 4) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 2) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 15) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 5) Nat :: ["A"(3, 0)] -(0)-> "A"(3, 14) Sub :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) Sub :: ["A"(3, 3) x "A"(3, 3)] -(0)-> "A"(0, 3) Succ :: ["A"(3, 0)] -(3)-> "A"(3, 0) Zero :: [] -(0)-> "A"(3, 0) Zero :: [] -(0)-> "A"(11, 8) cond_eval_expr_1 :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) cond_eval_expr_2 :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) cond_eval_expr_3 :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0) eval#1 :: ["A"(3, 0)] -(0)-> "A"(3, 0) cond_eval_expr_1# :: ["A"(3, 0) x "A"(0, 3)] -(0)-> "A"(1, 3) cond_eval_expr_2# :: ["A"(3, 0) x "A"(3, 3)] -(0)-> "A"(1, 1) cond_eval_expr_3# :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(5, 1) eval#1# :: ["A"(0, 3)] -(0)-> "A"(5, 0) c_1 :: ["A"(0, 0)] -(0)-> "A"(4, 14) c_2 :: ["A"(3, 0)] -(0)-> "A"(9, 3) c_3 :: ["A"(5, 0) x "A"(0, 0)] -(0)-> "A"(3, 2) c_4 :: ["A"(0, 0)] -(0)-> "A"(14, 9) c_5 :: ["A"(0, 0)] -(0)-> "A"(12, 4) c_7 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(7, 14) c_9 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 2) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Add_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "Add_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1) "Nat_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "Nat_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "Sub_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "Sub_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "Succ_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "Succ_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "Zero_A" :: [] -(0)-> "A"(1, 0) "Zero_A" :: [] -(0)-> "A"(0, 1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_2_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) "c_4_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_4_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_5_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_5_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) 2. Weak: WORST_CASE(?,O(n^2))